Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update lean toolchain after lake update #354

Merged
merged 2 commits into from
Nov 14, 2023

Conversation

mhuisi
Copy link
Collaborator

@mhuisi mhuisi commented Nov 10, 2023

This PR adjusts the Project: Update Dependency command so that it updates the toolchain after running lake update. This was prompted by the introduction of a post-update hook in leanprover-community/mathlib4#8243 that automatically updates the toolchain.

With the post-update hook and asking to update the toolchain before running lake update, a user decision of "Do not update the toolchain" would be ignored for projects downstream of Mathlib, as the post-update hook will update the toolchain regardless of the user choice. Asking to update the toolchain (if it changed) after lake update ensures users do not see a misleading dialog.

One caveat is that this means that we will now run lake update with the Lean version of the project itself, not the Lean version of its dependency.

Another change induced by switching the order of operations is that we can now read the toolchain from lake-packages instead of fetching it from raw.githubusercontent.com.

@mhuisi mhuisi merged commit ba5c660 into leanprover:master Nov 14, 2023
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants